def f : (α : Type) × α → Nat
 | ⟨_, true⟩ => 1
 | _ => 2
